not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(not1(not1(x))), not1(not1(not1(y))))
not1(and2(x, y)) -> or2(not1(not1(not1(x))), not1(not1(not1(y))))
↳ QTRS
↳ DependencyPairsProof
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(not1(not1(x))), not1(not1(not1(y))))
not1(and2(x, y)) -> or2(not1(not1(not1(x))), not1(not1(not1(y))))
NOT1(and2(x, y)) -> NOT1(x)
NOT1(and2(x, y)) -> NOT1(not1(x))
NOT1(and2(x, y)) -> NOT1(y)
NOT1(or2(x, y)) -> NOT1(x)
NOT1(or2(x, y)) -> NOT1(not1(not1(x)))
NOT1(or2(x, y)) -> NOT1(y)
NOT1(and2(x, y)) -> NOT1(not1(not1(y)))
NOT1(or2(x, y)) -> NOT1(not1(x))
NOT1(and2(x, y)) -> NOT1(not1(y))
NOT1(or2(x, y)) -> NOT1(not1(y))
NOT1(and2(x, y)) -> NOT1(not1(not1(x)))
NOT1(or2(x, y)) -> NOT1(not1(not1(y)))
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(not1(not1(x))), not1(not1(not1(y))))
not1(and2(x, y)) -> or2(not1(not1(not1(x))), not1(not1(not1(y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
NOT1(and2(x, y)) -> NOT1(x)
NOT1(and2(x, y)) -> NOT1(not1(x))
NOT1(and2(x, y)) -> NOT1(y)
NOT1(or2(x, y)) -> NOT1(x)
NOT1(or2(x, y)) -> NOT1(not1(not1(x)))
NOT1(or2(x, y)) -> NOT1(y)
NOT1(and2(x, y)) -> NOT1(not1(not1(y)))
NOT1(or2(x, y)) -> NOT1(not1(x))
NOT1(and2(x, y)) -> NOT1(not1(y))
NOT1(or2(x, y)) -> NOT1(not1(y))
NOT1(and2(x, y)) -> NOT1(not1(not1(x)))
NOT1(or2(x, y)) -> NOT1(not1(not1(y)))
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(not1(not1(x))), not1(not1(not1(y))))
not1(and2(x, y)) -> or2(not1(not1(not1(x))), not1(not1(not1(y))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NOT1(and2(x, y)) -> NOT1(x)
NOT1(and2(x, y)) -> NOT1(not1(x))
NOT1(and2(x, y)) -> NOT1(y)
NOT1(or2(x, y)) -> NOT1(x)
NOT1(or2(x, y)) -> NOT1(not1(not1(x)))
NOT1(or2(x, y)) -> NOT1(y)
NOT1(and2(x, y)) -> NOT1(not1(not1(y)))
NOT1(or2(x, y)) -> NOT1(not1(x))
NOT1(and2(x, y)) -> NOT1(not1(y))
NOT1(or2(x, y)) -> NOT1(not1(y))
NOT1(and2(x, y)) -> NOT1(not1(not1(x)))
NOT1(or2(x, y)) -> NOT1(not1(not1(y)))
POL(NOT1(x1)) = 2·x1
POL(and2(x1, x2)) = 1 + 2·x1 + 2·x2
POL(not1(x1)) = x1
POL(or2(x1, x2)) = 1 + 2·x1 + 2·x2
not1(or2(x, y)) -> and2(not1(not1(not1(x))), not1(not1(not1(y))))
not1(not1(x)) -> x
not1(and2(x, y)) -> or2(not1(not1(not1(x))), not1(not1(not1(y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(not1(not1(x))), not1(not1(not1(y))))
not1(and2(x, y)) -> or2(not1(not1(not1(x))), not1(not1(not1(y))))